Nuprl Lemma : R-and-left 11,40

AB:es_realizer{i:l}, P:(ES{i}{i'}).
R-Feasible{i:l}(A B ||-{i} es.P(es R-compat{i:l}(AB A  B ||-{i} es.P(es
latex


DefinitionsP & Q, True, xt(x), t  T, x(s), P  Q, , x:AB(x)
LemmasRplus wf, R-implies-rule, R-true-rule, es realizer wf, R-Feasible wf, event system wf, R-realizes wf, R-compat wf, true wf, R-and-rule

origin